es:event_system{i:l}, l:IdLnk, tg:Id, e:es-E(es).
(es-kind(es; e) = rcv(l,tg)  Knd)
 guard(((es-isrcv(es; e))
 guard(c ((es-lnk(es; e) = l)  (es-tag(es; e) = tg)  (loc(es-sender(es; e)) = source(l)  Id)))
 guard() 

latex

Definitions	x:A. B(x), P  Q, es-isrcv(es; e), es-lnk(es; e), es-tag(es; e), t  T, prop{i:l}, rcv(l,tg), guard(T), A c B, b, isrcv(k), P  Q, lnk(k), tag(k), isl(x), t.1, outl(x), t.2, tt, if b then t else f fi , True, ff, T, sq_type(T), Knd, decidable(P), P  Q, False, ||as||, Y, locl(a)
Lemmas	Knd wf, es-kind wf, rcv wf, es-E wf, Id wf, IdLnk wf, event system wf, true wf, false wf, decidable equal Id, es-loc wf, es-sender wf, lsrc wf, es-axioms, es-lnk wf, not wf, squash wf, not rcv locl, es-index wf, length wf1, es-Msgl wf, length wf2, guard wf, assert wf, isrcv wf